Coyotos Secure Operating System

I found a new interesting new operating systemCoyotos Secure Operating System, it is designed from the ground up not only to be secure but to be verifiably secure, and implemented in a way that is also verifiably secure creating their own Lisp like language, called BitC, to do it. The designer of this language has also designed another called E, which is quite Python like and also secure by design with a built in Capability system. It has been implemented on the Java Virtual Machine so I'll download a copy and see what it is like.